i, j:. ((i = j))  ((i = j) ~ ff) 

latex

Up	sqequal 1, sqequal 1
Definitions	, t  T, P  Q, x:A. B(x), {T}, SQType(T), P & Q, P  Q, P  Q
Lemmas	not wf, bool sq, assert of eq int, not functionality wrt iff, assert of bnot, eqff to assert, bnot wf, assert wf, bfalse wf, eq int wf, bool wf, iff transitivity